我如何将这些更改为 NuSMV 模型中的 CTL SPEC？

Question

我需要帮助编写这些 CTL。我还不太明白如何用 NuSMV 格式编写，希望我的代码对你有意义，因为它是不完整的 atm。

2)如果一个进程在等待，它最终会到达它的临界区

3)两个进程必须'take turns'进入临界区

4)一个进程有可能连续两次进入临界区（在另一个进程之前）。

5) 进程 1 连续进入临界区将至少间隔 n 个周期，其中 n 是某个常数。你应该为 n 选择一个合适的值，并且这个应该被验证（即，没有被证明）。

6)2 个您选择的更重要的属性

MODULE thread1(flag2,turn)
VAR
   state : {W0,F1,W1,T1,F2,Wait,F3,C1,T2,F4};
   flag1 : boolean;

ASSIGN
   init(state) := W0;
   next(state) :=
case
   state = W0                 : F1;  
   state = F1                 : W1;  
   state = W1 & flag2         : T1; 
   (state = W1) & !flag2      : C1;  
   (state = T1)&(turn = 2)    : F2;  
   (state = T1)&(turn != 2)   : W1;  
   (state = F2)               : Wait; 
   (state = Wait)&(turn = 1)  : F3;   
   (state = Wait)&(turn != 1) : Wait; 
   (state = F3)               : W1; 
   (state = C1)               : T2; 
   (state = T2)               : F4; 
   (state = F4)               : W0;
    TRUE : state;
esac;

init(flag1) := FALSE;
next(flag1) := 
case
   state = F1 | state = F3 : TRUE;  
   state = F2 | state = F4 : FALSE; 
   TRUE                    : flag1;
esac;

DEFINE
  critical := (state = C1);
  trying := (state = F1 | state = W1 | state = T1 | state = F2 |     state = Wait | state = F3);  

MODULE thread2(flag1,turn)
VAR
   state1 : {N0,N1,N2,N3,N4,Wait1,N5,Critical1,N7,N8};
   flag2 : boolean;

ASSIGN
   init(state1) := N0;
   next(state1) :=
case
   (state1 = N0)               : N1;  
   (state1 = N1)               : N2;  
   (state1 = N2) & flag1       : N3;  
   (state1 = N2) & !flag1      : Critical1;
   (state1 = N3) & (turn = 1)  : N4;  
   (state1 = N3) & (turn != 2) : N2;  
   (state1 = F4)               : Wait1; 
   (state1 = Wait1)&(turn = 2) : N5;   
   (state1 = Wait1)&(turn != 2): Wait1; 
   (state1 = N5)               : N2; 
   (state1 = Critical1)        : N7; 
   (state1 = N7)               : N8;
   (state1 = N8)               : N0;
    TRUE : state1;
esac;

init(flag2) := FALSE;
next(flag2) := 
case
   state1 = N1 | state1 = N5 : TRUE;  
   state1 = N4 | state1 = N8 : FALSE;
   TRUE                    : flag2;
esac;

DEFINE
  critical := (state1 = Critical1);
  trying := (state1 = N1 | state1 = N2 | state1 = N3 | state1 = N4 |     state1 = Wait1 | state1 = N5);  

MODULE main

VAR

turn: {1, 2};
proc1: process thread1(proc2.flag2,turn);
proc2: process thread2(proc1.flag1,turn);

ASSIGN

init(turn) := 1;
next(turn) := 
case
   proc1.state = T2 : 2;
   proc2.state1 = N7 : 1;
   TRUE : turn;
esac;

SPEC 

AG !(proc1.critical & proc2.critical); 
--two processes are never in the critical section at the same time

SPEC 
AG (proc1.trying -> AF proc1.critical);

Answer 1

注意：在一个答案中给你全面介绍CTL是很不现实的。除了 this quick and dirty course on NuSMV/nuXmv, you might benefit from looking at these slides，它提供了 CTL 模型检查的理论背景。

CTL 操作员

假设为简单起见，您的程序具有唯一 初始状态。

CTL 运算符的语义如下：

AF P: 在所有个可能的执行路径中，迟早 P 将是 true.
AG P: 在所有个可能的执行路径中，P是总是真.
AX P: 在所有个可能的执行路径中，处于下一个状态P 是真.
A[P U Q]：在所有个可能的执行路径中，P 是 true * until Q 是 true (至少一次）。
EF P: 在至少一个执行路径中，迟早 P 将是 true.
EG P: 在至少一个执行路径中，P是总是真.
EX P: 在至少一个执行路径中，处于下一个状态P 是 true.
E[P U Q]：在至少一个执行路径中，P是true * until Q 是 true （至少一次） .

*: until 是 true 也在一条路径上 P 永远不会 true，前提是Q立即验证。 [另见：weak/strong直到]

如果你有多个 初始状态，那么CTL 属性如果每个 初始状态 .

为 true，则成立

属性：

请注意，由于您的 NuSMV 模型目前已损坏，这似乎是一项作业，我将为您提供一个 伪代码 版本的属性，并留给您让它们适合您自己的代码。

如果一个进程正在等待，那么它最终会到达它的临界区
```
CTLSPEC AG (proc1.waiting -> AF proc1.critical);
```
解释：括号中的内容准确编码了您阅读的句子。我添加了 AG，因为属性必须明确适用于模型中的每个可能状态。如果您省略它，那么模型检查器将简单地测试 proc1.waiting -> AF proc1.critical 在您的初始状态下是否 true。
两个进程必须'take turns'进入临界区
```
CTLSPEC AG ((proc1.critical -> AX A[!proc1.critical U proc2.critical]) &
           (proc2.critical -> AX A[!proc2.critical U proc1.critical]));
```
解释： 让我假设此编码有效，因为 proc1 和 proc2 都保留在临界区中只有一个状态。 proc1.critical -> AX A[!proc1.critical U proc2.critical]的思路如下："if process 1 is in the critical section, then starting from the next state process 1 will never be in the critical section (again) until when process 2 is in the critical section".
一个进程有可能连续两次进入临界区（在另一个进程之前）。
```
CTLSPEC EF (proc1.critical -> EX A[!proc2.critical U proc1.critical]);
```
说明：与上一个类似。这里我使用 EF 因为它足以满足属性 holds 一次。
进程 1 连续进入临界区将至少间隔 n 个周期，其中 n 是某个常数。你应该为 n 选择一个合适的值，并且这个应该被验证（即，没有被证明）。

编辑： 我删除了这个编码，因为转念一想我写的公式比要求的强多。但是，我认为不可能使用 E 运算符来削弱它，因为它会变得比要求的弱得多。目前我想不出一个可能的替代方案，除了修改你的模型来计算周期的数量，不管那是什么意思。

我如何将这些更改为 NuSMV 模型中的 CTL SPEC？

How can i change these into CTL SPEC in NuSMV model?

logic

model-checking

model

ctl

nusmv